(set-info :source |fuzzsmt|)
(set-info :smt-lib-version 2.0)
(set-info :category "random")
(set-info :status unknown)
(set-logic QF_UFBV)
(declare-fun f0 ( (_ BitVec 1)) (_ BitVec 96))
(declare-fun f1 ( (_ BitVec 17) (_ BitVec 24) (_ BitVec 68)) (_ BitVec 109))
(declare-fun p0 ( (_ BitVec 33) (_ BitVec 33)) Bool)
(declare-fun v0 () (_ BitVec 22))
(declare-fun v1 () (_ BitVec 90))
(declare-fun v2 () (_ BitVec 75))
(declare-fun v3 () (_ BitVec 74))
(assert (let ((e4(_ bv77830107773253007339250731326514 106)))
(let ((e5(_ bv7 7)))
(let ((e6 (f1 ((_ extract 48 32) v2) ((_ extract 73 50) v2) ((_ extract 95 28) e4))))
(let ((e7 (ite (p0 ((_ extract 105 73) e6) ((_ extract 84 52) e4)) (_ bv1 1) (_ bv0 1))))
(let ((e8 (bvsub v2 ((_ zero_extend 1) v3))))
(let ((e9 (f0 ((_ extract 0 0) v0))))
(let ((e10 (bvmul e4 ((_ zero_extend 10) e9))))
(let ((e11 ((_ rotate_left 1) e5)))
(let ((e12 (ite (= e11 ((_ zero_extend 6) e7)) (_ bv1 1) (_ bv0 1))))
(let ((e13 ((_ rotate_right 0) v0)))
(let ((e14 (bvlshr e6 ((_ sign_extend 3) e10))))
(let ((e15 ((_ rotate_left 4) e11)))
(let ((e16 (ite (bvsgt e14 ((_ sign_extend 13) e9)) (_ bv1 1) (_ bv0 1))))
(let ((e17 (ite (p0 ((_ zero_extend 11) v0) ((_ extract 44 12) e8)) (_ bv1 1) (_ bv0 1))))
(let ((e18 (f1 ((_ extract 99 83) e14) ((_ extract 72 49) v3) ((_ sign_extend 61) e11))))
(let ((e19 (bvshl ((_ zero_extend 108) e12) e18)))
(let ((e20 ((_ sign_extend 35) v1)))
(let ((e21 (p0 ((_ zero_extend 32) e12) ((_ sign_extend 32) e12))))
(let ((e22 (bvult ((_ zero_extend 102) e15) e19)))
(let ((e23 (bvugt ((_ zero_extend 35) v3) e18)))
(let ((e24 (= ((_ sign_extend 102) e15) e14)))
(let ((e25 (bvsge ((_ zero_extend 15) e5) e13)))
(let ((e26 (distinct e20 ((_ zero_extend 124) e7))))
(let ((e27 (bvule e15 e5)))
(let ((e28 (bvsgt e14 ((_ zero_extend 108) e17))))
(let ((e29 (distinct e13 ((_ zero_extend 21) e12))))
(let ((e30 (bvslt ((_ zero_extend 10) e9) e10)))
(let ((e31 (bvugt e10 ((_ sign_extend 16) v1))))
(let ((e32 (bvsgt v1 ((_ zero_extend 89) e16))))
(let ((e33 (bvslt ((_ zero_extend 6) e7) e5)))
(let ((e34 (= e17 e16)))
(let ((e35 (p0 ((_ sign_extend 32) e16) ((_ extract 66 34) v2))))
(let ((e36 (bvuge ((_ sign_extend 21) e7) e13)))
(let ((e37 (bvule e10 ((_ sign_extend 84) v0))))
(let ((e38 (bvult e10 ((_ sign_extend 105) e7))))
(let ((e39 (bvsle e13 ((_ zero_extend 15) e15))))
(let ((e40 (bvule ((_ zero_extend 73) e17) v3)))
(let ((e41 (bvsle ((_ sign_extend 74) e17) e8)))
(let ((e42 (bvsgt ((_ zero_extend 3) e4) e18)))
(let ((e43 (bvugt e8 ((_ sign_extend 74) e12))))
(let ((e44 (bvsgt e8 ((_ zero_extend 68) e11))))
(let ((e45 (distinct e8 ((_ sign_extend 1) v3))))
(let ((e46 (distinct ((_ sign_extend 34) v2) e19)))
(let ((e47 (distinct v3 ((_ zero_extend 52) e13))))
(let ((e48 (= e6 ((_ sign_extend 102) e11))))
(let ((e49 (= e46 e26)))
(let ((e50 (= e39 e40)))
(let ((e51 (or e37 e32)))
(let ((e52 (ite e21 e33 e35)))
(let ((e53 (xor e49 e27)))
(let ((e54 (ite e52 e23 e30)))
(let ((e55 (and e54 e54)))
(let ((e56 (=> e47 e44)))
(let ((e57 (ite e29 e56 e31)))
(let ((e58 (not e24)))
(let ((e59 (not e53)))
(let ((e60 (xor e22 e51)))
(let ((e61 (= e48 e41)))
(let ((e62 (or e61 e45)))
(let ((e63 (=> e43 e55)))
(let ((e64 (= e34 e25)))
(let ((e65 (not e59)))
(let ((e66 (and e58 e63)))
(let ((e67 (=> e60 e42)))
(let ((e68 (=> e28 e50)))
(let ((e69 (=> e65 e67)))
(let ((e70 (and e68 e64)))
(let ((e71 (= e66 e70)))
(let ((e72 (ite e69 e36 e57)))
(let ((e73 (xor e72 e38)))
(let ((e74 (not e62)))
(let ((e75 (xor e71 e74)))
(let ((e76 (not e75)))
(let ((e77 (=> e76 e76)))
(let ((e78 (= e73 e77)))
e78
))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))

(check-sat)
